Left Termination proof of /tmp/tmpLu-YsH/zebra.pl

Left Termination of the query pattern zebra_in_7(a, a, a, a, a, a, a) w.r.t. the given Prolog program could successfully be proven:

↳ Prolog

  ↳ PrologToPiTRSProof

Clauses:

zebra(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) :- ','(eq(Englishman, Red), ','(eq(Spaniard, Dog), ','(eq(Green, Coffee), ','(eq(Ukrainian, Tea), ','(to_the_right(Green, Ivory), ','(eq(Winston, Snails), ','(eq(Kool, Yellow), ','(eq(Milk, third), ','(eq(Norwegian, first), ','(next_to(Fox, Chesterfield), ','(next_to(Horse, Kool), ','(eq(Lucky, Juice), ','(eq(Japanese, Parliament), ','(next_to(Norwegian, Blue), ','(houses(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, [])))))), ','(houses(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, [])))))), ','(houses(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, [])))))), ','(houses(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, [])))))), houses(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, [])))))))))))))))))))))))).
houses(Prop) :- domain(Prop, .(first, .(second, .(third, .(fourth, .(fifth, [])))))).
domain([], X).
domain(.(X, Rest), Domain) :- ','(select(X, Domain, NewDomain), domain(Rest, NewDomain)).
select(X, .(X, R), R).
select(X, .(Y, R), .(Y, Rest)) :- select(X, R, Rest).
next_to(fifth, fourth).
next_to(fourth, fifth).
next_to(fourth, third).
next_to(third, fourth).
next_to(third, second).
next_to(second, third).
next_to(second, first).
next_to(first, second).
to_the_right(fifth, fourth).
to_the_right(fourth, third).
to_the_right(third, second).
to_the_right(second, first).
eq(X, X).

Queries:

zebra(a,a,a,a,a,a,a).

We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
zebra_in: (f,f,f,f,f,f,f)
houses_in: (f)
domain_in: (f,b)
select_in: (f,b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

zebra_in_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) → U1_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_in_aa(Englishman, Red))
eq_in_aa(X, X) → eq_out_aa(X, X)
U1_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_out_aa(Englishman, Red)) → U2_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_in_aa(Spaniard, Dog))
U2_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_out_aa(Spaniard, Dog)) → U3_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_in_aa(Green, Coffee))
U3_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_out_aa(Green, Coffee)) → U4_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_in_aa(Ukrainian, Tea))
U4_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_out_aa(Ukrainian, Tea)) → U5_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_in_aa(Green, Ivory))
to_the_right_in_aa(fifth, fourth) → to_the_right_out_aa(fifth, fourth)
to_the_right_in_aa(fourth, third) → to_the_right_out_aa(fourth, third)
to_the_right_in_aa(third, second) → to_the_right_out_aa(third, second)
to_the_right_in_aa(second, first) → to_the_right_out_aa(second, first)
U5_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_out_aa(Green, Ivory)) → U6_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_in_aa(Winston, Snails))
U6_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_out_aa(Winston, Snails)) → U7_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_in_aa(Kool, Yellow))
U7_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_out_aa(Kool, Yellow)) → U8_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_in_ag(Milk, third))
eq_in_ag(X, X) → eq_out_ag(X, X)
U8_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_out_ag(Milk, third)) → U9_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_in_ag(Norwegian, first))
U9_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_out_ag(Norwegian, first)) → U10_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_in_aa(Fox, Chesterfield))
next_to_in_aa(fifth, fourth) → next_to_out_aa(fifth, fourth)
next_to_in_aa(fourth, fifth) → next_to_out_aa(fourth, fifth)
next_to_in_aa(fourth, third) → next_to_out_aa(fourth, third)
next_to_in_aa(third, fourth) → next_to_out_aa(third, fourth)
next_to_in_aa(third, second) → next_to_out_aa(third, second)
next_to_in_aa(second, third) → next_to_out_aa(second, third)
next_to_in_aa(second, first) → next_to_out_aa(second, first)
next_to_in_aa(first, second) → next_to_out_aa(first, second)
U10_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_out_aa(Fox, Chesterfield)) → U11_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_in_aa(Horse, Kool))
U11_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_out_aa(Horse, Kool)) → U12_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_in_aa(Lucky, Juice))
U12_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_out_aa(Lucky, Juice)) → U13_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_in_aa(Japanese, Parliament))
U13_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_out_aa(Japanese, Parliament)) → U14_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_in_ga(Norwegian, Blue))
next_to_in_ga(fifth, fourth) → next_to_out_ga(fifth, fourth)
next_to_in_ga(fourth, fifth) → next_to_out_ga(fourth, fifth)
next_to_in_ga(fourth, third) → next_to_out_ga(fourth, third)
next_to_in_ga(third, fourth) → next_to_out_ga(third, fourth)
next_to_in_ga(third, second) → next_to_out_ga(third, second)
next_to_in_ga(second, third) → next_to_out_ga(second, third)
next_to_in_ga(second, first) → next_to_out_ga(second, first)
next_to_in_ga(first, second) → next_to_out_ga(first, second)
U14_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_out_ga(Norwegian, Blue)) → U15_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_a(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, [])))))))
houses_in_a(Prop) → U20_a(Prop, domain_in_ag(Prop, .(first, .(second, .(third, .(fourth, .(fifth, [])))))))
domain_in_ag([], X) → domain_out_ag([], X)
domain_in_ag(.(X, Rest), Domain) → U21_ag(X, Rest, Domain, select_in_aga(X, Domain, NewDomain))
select_in_aga(X, .(X, R), R) → select_out_aga(X, .(X, R), R)
select_in_aga(X, .(Y, R), .(Y, Rest)) → U23_aga(X, Y, R, Rest, select_in_aga(X, R, Rest))
U23_aga(X, Y, R, Rest, select_out_aga(X, R, Rest)) → select_out_aga(X, .(Y, R), .(Y, Rest))
U21_ag(X, Rest, Domain, select_out_aga(X, Domain, NewDomain)) → U22_ag(X, Rest, Domain, domain_in_ag(Rest, NewDomain))
U22_ag(X, Rest, Domain, domain_out_ag(Rest, NewDomain)) → domain_out_ag(.(X, Rest), Domain)
U20_a(Prop, domain_out_ag(Prop, .(first, .(second, .(third, .(fourth, .(fifth, []))))))) → houses_out_a(Prop)
U15_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_a(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))) → U16_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_a(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, [])))))))
U16_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_a(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))) → U17_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_in_a(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, [])))))))
U17_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_out_a(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))) → U18_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_in_a(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, [])))))))
U18_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_out_a(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))) → U19_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_in_a(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, [])))))))
U19_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_out_a(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, []))))))) → zebra_out_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

zebra_in_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) → U1_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_in_aa(Englishman, Red))
eq_in_aa(X, X) → eq_out_aa(X, X)
U1_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_out_aa(Englishman, Red)) → U2_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_in_aa(Spaniard, Dog))
U2_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_out_aa(Spaniard, Dog)) → U3_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_in_aa(Green, Coffee))
U3_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_out_aa(Green, Coffee)) → U4_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_in_aa(Ukrainian, Tea))
U4_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_out_aa(Ukrainian, Tea)) → U5_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_in_aa(Green, Ivory))
to_the_right_in_aa(fifth, fourth) → to_the_right_out_aa(fifth, fourth)
to_the_right_in_aa(fourth, third) → to_the_right_out_aa(fourth, third)
to_the_right_in_aa(third, second) → to_the_right_out_aa(third, second)
to_the_right_in_aa(second, first) → to_the_right_out_aa(second, first)
U5_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_out_aa(Green, Ivory)) → U6_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_in_aa(Winston, Snails))
U6_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_out_aa(Winston, Snails)) → U7_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_in_aa(Kool, Yellow))
U7_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_out_aa(Kool, Yellow)) → U8_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_in_ag(Milk, third))
eq_in_ag(X, X) → eq_out_ag(X, X)
U8_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_out_ag(Milk, third)) → U9_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_in_ag(Norwegian, first))
U9_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_out_ag(Norwegian, first)) → U10_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_in_aa(Fox, Chesterfield))
next_to_in_aa(fifth, fourth) → next_to_out_aa(fifth, fourth)
next_to_in_aa(fourth, fifth) → next_to_out_aa(fourth, fifth)
next_to_in_aa(fourth, third) → next_to_out_aa(fourth, third)
next_to_in_aa(third, fourth) → next_to_out_aa(third, fourth)
next_to_in_aa(third, second) → next_to_out_aa(third, second)
next_to_in_aa(second, third) → next_to_out_aa(second, third)
next_to_in_aa(second, first) → next_to_out_aa(second, first)
next_to_in_aa(first, second) → next_to_out_aa(first, second)
U10_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_out_aa(Fox, Chesterfield)) → U11_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_in_aa(Horse, Kool))
U11_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_out_aa(Horse, Kool)) → U12_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_in_aa(Lucky, Juice))
U12_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_out_aa(Lucky, Juice)) → U13_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_in_aa(Japanese, Parliament))
U13_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_out_aa(Japanese, Parliament)) → U14_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_in_ga(Norwegian, Blue))
next_to_in_ga(fifth, fourth) → next_to_out_ga(fifth, fourth)
next_to_in_ga(fourth, fifth) → next_to_out_ga(fourth, fifth)
next_to_in_ga(fourth, third) → next_to_out_ga(fourth, third)
next_to_in_ga(third, fourth) → next_to_out_ga(third, fourth)
next_to_in_ga(third, second) → next_to_out_ga(third, second)
next_to_in_ga(second, third) → next_to_out_ga(second, third)
next_to_in_ga(second, first) → next_to_out_ga(second, first)
next_to_in_ga(first, second) → next_to_out_ga(first, second)
U14_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_out_ga(Norwegian, Blue)) → U15_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_a(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, [])))))))
houses_in_a(Prop) → U20_a(Prop, domain_in_ag(Prop, .(first, .(second, .(third, .(fourth, .(fifth, [])))))))
domain_in_ag([], X) → domain_out_ag([], X)
domain_in_ag(.(X, Rest), Domain) → U21_ag(X, Rest, Domain, select_in_aga(X, Domain, NewDomain))
select_in_aga(X, .(X, R), R) → select_out_aga(X, .(X, R), R)
select_in_aga(X, .(Y, R), .(Y, Rest)) → U23_aga(X, Y, R, Rest, select_in_aga(X, R, Rest))
U23_aga(X, Y, R, Rest, select_out_aga(X, R, Rest)) → select_out_aga(X, .(Y, R), .(Y, Rest))
U21_ag(X, Rest, Domain, select_out_aga(X, Domain, NewDomain)) → U22_ag(X, Rest, Domain, domain_in_ag(Rest, NewDomain))
U22_ag(X, Rest, Domain, domain_out_ag(Rest, NewDomain)) → domain_out_ag(.(X, Rest), Domain)
U20_a(Prop, domain_out_ag(Prop, .(first, .(second, .(third, .(fourth, .(fifth, []))))))) → houses_out_a(Prop)
U15_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_a(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))) → U16_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_a(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, [])))))))
U16_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_a(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))) → U17_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_in_a(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, [])))))))
U17_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_out_a(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))) → U18_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_in_a(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, [])))))))
U18_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_out_a(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))) → U19_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_in_a(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, [])))))))
U19_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_out_a(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, []))))))) → zebra_out_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water)

ZEBRA_IN_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) → U1_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_in_aa(Englishman, Red))
ZEBRA_IN_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) → EQ_IN_AA(Englishman, Red)
U1_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_out_aa(Englishman, Red)) → U2_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_in_aa(Spaniard, Dog))
U1_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_out_aa(Englishman, Red)) → EQ_IN_AA(Spaniard, Dog)
U2_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_out_aa(Spaniard, Dog)) → U3_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_in_aa(Green, Coffee))
U2_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_out_aa(Spaniard, Dog)) → EQ_IN_AA(Green, Coffee)
U3_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_out_aa(Green, Coffee)) → U4_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_in_aa(Ukrainian, Tea))
U3_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_out_aa(Green, Coffee)) → EQ_IN_AA(Ukrainian, Tea)
U4_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_out_aa(Ukrainian, Tea)) → U5_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_in_aa(Green, Ivory))
U4_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_out_aa(Ukrainian, Tea)) → TO_THE_RIGHT_IN_AA(Green, Ivory)
U5_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_out_aa(Green, Ivory)) → U6_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_in_aa(Winston, Snails))
U5_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_out_aa(Green, Ivory)) → EQ_IN_AA(Winston, Snails)
U6_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_out_aa(Winston, Snails)) → U7_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_in_aa(Kool, Yellow))
U6_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_out_aa(Winston, Snails)) → EQ_IN_AA(Kool, Yellow)
U7_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_out_aa(Kool, Yellow)) → U8_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_in_ag(Milk, third))
U7_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_out_aa(Kool, Yellow)) → EQ_IN_AG(Milk, third)
U8_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_out_ag(Milk, third)) → U9_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_in_ag(Norwegian, first))
U8_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_out_ag(Milk, third)) → EQ_IN_AG(Norwegian, first)
U9_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_out_ag(Norwegian, first)) → U10_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_in_aa(Fox, Chesterfield))
U9_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_out_ag(Norwegian, first)) → NEXT_TO_IN_AA(Fox, Chesterfield)
U10_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_out_aa(Fox, Chesterfield)) → U11_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_in_aa(Horse, Kool))
U10_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_out_aa(Fox, Chesterfield)) → NEXT_TO_IN_AA(Horse, Kool)
U11_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_out_aa(Horse, Kool)) → U12_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_in_aa(Lucky, Juice))
U11_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_out_aa(Horse, Kool)) → EQ_IN_AA(Lucky, Juice)
U12_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_out_aa(Lucky, Juice)) → U13_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_in_aa(Japanese, Parliament))
U12_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_out_aa(Lucky, Juice)) → EQ_IN_AA(Japanese, Parliament)
U13_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_out_aa(Japanese, Parliament)) → U14_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_in_ga(Norwegian, Blue))
U13_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_out_aa(Japanese, Parliament)) → NEXT_TO_IN_GA(Norwegian, Blue)
U14_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_out_ga(Norwegian, Blue)) → U15_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_a(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, [])))))))
U14_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_out_ga(Norwegian, Blue)) → HOUSES_IN_A(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))
HOUSES_IN_A(Prop) → U20_A(Prop, domain_in_ag(Prop, .(first, .(second, .(third, .(fourth, .(fifth, [])))))))
HOUSES_IN_A(Prop) → DOMAIN_IN_AG(Prop, .(first, .(second, .(third, .(fourth, .(fifth, []))))))
DOMAIN_IN_AG(.(X, Rest), Domain) → U21_AG(X, Rest, Domain, select_in_aga(X, Domain, NewDomain))
DOMAIN_IN_AG(.(X, Rest), Domain) → SELECT_IN_AGA(X, Domain, NewDomain)
SELECT_IN_AGA(X, .(Y, R), .(Y, Rest)) → U23_AGA(X, Y, R, Rest, select_in_aga(X, R, Rest))
SELECT_IN_AGA(X, .(Y, R), .(Y, Rest)) → SELECT_IN_AGA(X, R, Rest)
U21_AG(X, Rest, Domain, select_out_aga(X, Domain, NewDomain)) → U22_AG(X, Rest, Domain, domain_in_ag(Rest, NewDomain))
U21_AG(X, Rest, Domain, select_out_aga(X, Domain, NewDomain)) → DOMAIN_IN_AG(Rest, NewDomain)
U15_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_a(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))) → U16_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_a(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, [])))))))
U15_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_a(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))) → HOUSES_IN_A(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))
U16_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_a(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))) → U17_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_in_a(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, [])))))))
U16_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_a(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))) → HOUSES_IN_A(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))
U17_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_out_a(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))) → U18_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_in_a(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, [])))))))
U17_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_out_a(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))) → HOUSES_IN_A(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))
U18_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_out_a(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))) → U19_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_in_a(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, [])))))))
U18_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_out_a(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))) → HOUSES_IN_A(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, []))))))

The TRS R consists of the following rules:

zebra_in_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) → U1_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_in_aa(Englishman, Red))
eq_in_aa(X, X) → eq_out_aa(X, X)
U1_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_out_aa(Englishman, Red)) → U2_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_in_aa(Spaniard, Dog))
U2_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_out_aa(Spaniard, Dog)) → U3_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_in_aa(Green, Coffee))
U3_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_out_aa(Green, Coffee)) → U4_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_in_aa(Ukrainian, Tea))
U4_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_out_aa(Ukrainian, Tea)) → U5_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_in_aa(Green, Ivory))
to_the_right_in_aa(fifth, fourth) → to_the_right_out_aa(fifth, fourth)
to_the_right_in_aa(fourth, third) → to_the_right_out_aa(fourth, third)
to_the_right_in_aa(third, second) → to_the_right_out_aa(third, second)
to_the_right_in_aa(second, first) → to_the_right_out_aa(second, first)
U5_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_out_aa(Green, Ivory)) → U6_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_in_aa(Winston, Snails))
U6_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_out_aa(Winston, Snails)) → U7_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_in_aa(Kool, Yellow))
U7_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_out_aa(Kool, Yellow)) → U8_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_in_ag(Milk, third))
eq_in_ag(X, X) → eq_out_ag(X, X)
U8_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_out_ag(Milk, third)) → U9_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_in_ag(Norwegian, first))
U9_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_out_ag(Norwegian, first)) → U10_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_in_aa(Fox, Chesterfield))
next_to_in_aa(fifth, fourth) → next_to_out_aa(fifth, fourth)
next_to_in_aa(fourth, fifth) → next_to_out_aa(fourth, fifth)
next_to_in_aa(fourth, third) → next_to_out_aa(fourth, third)
next_to_in_aa(third, fourth) → next_to_out_aa(third, fourth)
next_to_in_aa(third, second) → next_to_out_aa(third, second)
next_to_in_aa(second, third) → next_to_out_aa(second, third)
next_to_in_aa(second, first) → next_to_out_aa(second, first)
next_to_in_aa(first, second) → next_to_out_aa(first, second)
U10_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_out_aa(Fox, Chesterfield)) → U11_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_in_aa(Horse, Kool))
U11_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_out_aa(Horse, Kool)) → U12_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_in_aa(Lucky, Juice))
U12_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_out_aa(Lucky, Juice)) → U13_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_in_aa(Japanese, Parliament))
U13_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_out_aa(Japanese, Parliament)) → U14_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_in_ga(Norwegian, Blue))
next_to_in_ga(fifth, fourth) → next_to_out_ga(fifth, fourth)
next_to_in_ga(fourth, fifth) → next_to_out_ga(fourth, fifth)
next_to_in_ga(fourth, third) → next_to_out_ga(fourth, third)
next_to_in_ga(third, fourth) → next_to_out_ga(third, fourth)
next_to_in_ga(third, second) → next_to_out_ga(third, second)
next_to_in_ga(second, third) → next_to_out_ga(second, third)
next_to_in_ga(second, first) → next_to_out_ga(second, first)
next_to_in_ga(first, second) → next_to_out_ga(first, second)
U14_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_out_ga(Norwegian, Blue)) → U15_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_a(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, [])))))))
houses_in_a(Prop) → U20_a(Prop, domain_in_ag(Prop, .(first, .(second, .(third, .(fourth, .(fifth, [])))))))
domain_in_ag([], X) → domain_out_ag([], X)
domain_in_ag(.(X, Rest), Domain) → U21_ag(X, Rest, Domain, select_in_aga(X, Domain, NewDomain))
select_in_aga(X, .(X, R), R) → select_out_aga(X, .(X, R), R)
select_in_aga(X, .(Y, R), .(Y, Rest)) → U23_aga(X, Y, R, Rest, select_in_aga(X, R, Rest))
U23_aga(X, Y, R, Rest, select_out_aga(X, R, Rest)) → select_out_aga(X, .(Y, R), .(Y, Rest))
U21_ag(X, Rest, Domain, select_out_aga(X, Domain, NewDomain)) → U22_ag(X, Rest, Domain, domain_in_ag(Rest, NewDomain))
U22_ag(X, Rest, Domain, domain_out_ag(Rest, NewDomain)) → domain_out_ag(.(X, Rest), Domain)
U20_a(Prop, domain_out_ag(Prop, .(first, .(second, .(third, .(fourth, .(fifth, []))))))) → houses_out_a(Prop)
U15_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_a(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))) → U16_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_a(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, [])))))))
U16_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_a(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))) → U17_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_in_a(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, [])))))))
U17_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_out_a(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))) → U18_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_in_a(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, [])))))))
U18_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_out_a(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))) → U19_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_in_a(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, [])))))))
U19_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_out_a(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, []))))))) → zebra_out_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water)

The argument filtering Pi contains the following mapping:
zebra_in_aaaaaaa(x1, x2, x3, x4, x5, x6, x7) = zebra_in_aaaaaaa
U1_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8) = U1_aaaaaaa(x8)
eq_in_aa(x1, x2) = eq_in_aa
eq_out_aa(x1, x2) = eq_out_aa
U2_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U2_aaaaaaa(x9)
U3_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = U3_aaaaaaa(x10)
U4_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) = U4_aaaaaaa(x12)
U5_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = U5_aaaaaaa(x13)
to_the_right_in_aa(x1, x2) = to_the_right_in_aa
to_the_right_out_aa(x1, x2) = to_the_right_out_aa(x1, x2)
U6_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14) = U6_aaaaaaa(x14)
U7_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16) = U7_aaaaaaa(x16)
U8_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18) = U8_aaaaaaa(x18)
eq_in_ag(x1, x2) = eq_in_ag(x2)
eq_out_ag(x1, x2) = eq_out_ag(x1)
third = third
U9_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U9_aaaaaaa(x19)
first = first
U10_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U10_aaaaaaa(x5, x19)
next_to_in_aa(x1, x2) = next_to_in_aa
next_to_out_aa(x1, x2) = next_to_out_aa(x1, x2)
U11_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21) = U11_aaaaaaa(x5, x21)
U12_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22) = U12_aaaaaaa(x5, x22)
U13_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24) = U13_aaaaaaa(x5, x24)
U14_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25) = U14_aaaaaaa(x5, x25)
next_to_in_ga(x1, x2) = next_to_in_ga(x1)
fifth = fifth
next_to_out_ga(x1, x2) = next_to_out_ga(x2)
fourth = fourth
second = second
U15_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21) = U15_aaaaaaa(x5, x21)
houses_in_a(x1) = houses_in_a
U20_a(x1, x2) = U20_a(x2)
domain_in_ag(x1, x2) = domain_in_ag(x2)
domain_out_ag(x1, x2) = domain_out_ag(x1)
U21_ag(x1, x2, x3, x4) = U21_ag(x4)
select_in_aga(x1, x2, x3) = select_in_aga(x2)
.(x1, x2) = .(x1, x2)
select_out_aga(x1, x2, x3) = select_out_aga(x1, x3)
U23_aga(x1, x2, x3, x4, x5) = U23_aga(x2, x5)
U22_ag(x1, x2, x3, x4) = U22_ag(x1, x4)
[] = []
houses_out_a(x1) = houses_out_a(x1)
U16_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21) = U16_aaaaaaa(x5, x21)
U17_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17) = U17_aaaaaaa(x1, x2, x3, x4, x5, x17)
U18_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) = U18_aaaaaaa(x1, x2, x3, x4, x5, x6, x12)
U19_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8) = U19_aaaaaaa(x1, x2, x3, x4, x5, x6, x8)
zebra_out_aaaaaaa(x1, x2, x3, x4, x5, x6, x7) = zebra_out_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)
ZEBRA_IN_AAAAAAA(x1, x2, x3, x4, x5, x6, x7) = ZEBRA_IN_AAAAAAA
U15_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21) = U15_AAAAAAA(x5, x21)
U3_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = U3_AAAAAAA(x10)
U11_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21) = U11_AAAAAAA(x5, x21)
U6_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14) = U6_AAAAAAA(x14)
U20_A(x1, x2) = U20_A(x2)
NEXT_TO_IN_GA(x1, x2) = NEXT_TO_IN_GA(x1)
U7_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16) = U7_AAAAAAA(x16)
U4_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) = U4_AAAAAAA(x12)
U23_AGA(x1, x2, x3, x4, x5) = U23_AGA(x2, x5)
EQ_IN_AA(x1, x2) = EQ_IN_AA
HOUSES_IN_A(x1) = HOUSES_IN_A
U9_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U9_AAAAAAA(x19)
U12_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22) = U12_AAAAAAA(x5, x22)
U5_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = U5_AAAAAAA(x13)
U14_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25) = U14_AAAAAAA(x5, x25)
U19_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8) = U19_AAAAAAA(x1, x2, x3, x4, x5, x6, x8)
SELECT_IN_AGA(x1, x2, x3) = SELECT_IN_AGA(x2)
U22_AG(x1, x2, x3, x4) = U22_AG(x1, x4)
U16_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21) = U16_AAAAAAA(x5, x21)
U17_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17) = U17_AAAAAAA(x1, x2, x3, x4, x5, x17)
NEXT_TO_IN_AA(x1, x2) = NEXT_TO_IN_AA
U1_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8) = U1_AAAAAAA(x8)
DOMAIN_IN_AG(x1, x2) = DOMAIN_IN_AG(x2)
EQ_IN_AG(x1, x2) = EQ_IN_AG(x2)
U13_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24) = U13_AAAAAAA(x5, x24)
U8_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18) = U8_AAAAAAA(x18)
U18_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) = U18_AAAAAAA(x1, x2, x3, x4, x5, x6, x12)
U2_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U2_AAAAAAA(x9)
U10_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U10_AAAAAAA(x5, x19)
U21_AG(x1, x2, x3, x4) = U21_AG(x4)
TO_THE_RIGHT_IN_AA(x1, x2) = TO_THE_RIGHT_IN_AA

We have to consider all (P,R,Pi)-chains

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

ZEBRA_IN_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) → U1_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_in_aa(Englishman, Red))
ZEBRA_IN_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) → EQ_IN_AA(Englishman, Red)
U1_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_out_aa(Englishman, Red)) → U2_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_in_aa(Spaniard, Dog))
U1_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_out_aa(Englishman, Red)) → EQ_IN_AA(Spaniard, Dog)
U2_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_out_aa(Spaniard, Dog)) → U3_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_in_aa(Green, Coffee))
U2_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_out_aa(Spaniard, Dog)) → EQ_IN_AA(Green, Coffee)
U3_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_out_aa(Green, Coffee)) → U4_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_in_aa(Ukrainian, Tea))
U3_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_out_aa(Green, Coffee)) → EQ_IN_AA(Ukrainian, Tea)
U4_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_out_aa(Ukrainian, Tea)) → U5_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_in_aa(Green, Ivory))
U4_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_out_aa(Ukrainian, Tea)) → TO_THE_RIGHT_IN_AA(Green, Ivory)
U5_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_out_aa(Green, Ivory)) → U6_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_in_aa(Winston, Snails))
U5_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_out_aa(Green, Ivory)) → EQ_IN_AA(Winston, Snails)
U6_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_out_aa(Winston, Snails)) → U7_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_in_aa(Kool, Yellow))
U6_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_out_aa(Winston, Snails)) → EQ_IN_AA(Kool, Yellow)
U7_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_out_aa(Kool, Yellow)) → U8_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_in_ag(Milk, third))
U7_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_out_aa(Kool, Yellow)) → EQ_IN_AG(Milk, third)
U8_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_out_ag(Milk, third)) → U9_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_in_ag(Norwegian, first))
U8_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_out_ag(Milk, third)) → EQ_IN_AG(Norwegian, first)
U9_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_out_ag(Norwegian, first)) → U10_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_in_aa(Fox, Chesterfield))
U9_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_out_ag(Norwegian, first)) → NEXT_TO_IN_AA(Fox, Chesterfield)
U10_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_out_aa(Fox, Chesterfield)) → U11_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_in_aa(Horse, Kool))
U10_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_out_aa(Fox, Chesterfield)) → NEXT_TO_IN_AA(Horse, Kool)
U11_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_out_aa(Horse, Kool)) → U12_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_in_aa(Lucky, Juice))
U11_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_out_aa(Horse, Kool)) → EQ_IN_AA(Lucky, Juice)
U12_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_out_aa(Lucky, Juice)) → U13_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_in_aa(Japanese, Parliament))
U12_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_out_aa(Lucky, Juice)) → EQ_IN_AA(Japanese, Parliament)
U13_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_out_aa(Japanese, Parliament)) → U14_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_in_ga(Norwegian, Blue))
U13_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_out_aa(Japanese, Parliament)) → NEXT_TO_IN_GA(Norwegian, Blue)
U14_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_out_ga(Norwegian, Blue)) → U15_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_a(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, [])))))))
U14_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_out_ga(Norwegian, Blue)) → HOUSES_IN_A(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))
HOUSES_IN_A(Prop) → U20_A(Prop, domain_in_ag(Prop, .(first, .(second, .(third, .(fourth, .(fifth, [])))))))
HOUSES_IN_A(Prop) → DOMAIN_IN_AG(Prop, .(first, .(second, .(third, .(fourth, .(fifth, []))))))
DOMAIN_IN_AG(.(X, Rest), Domain) → U21_AG(X, Rest, Domain, select_in_aga(X, Domain, NewDomain))
DOMAIN_IN_AG(.(X, Rest), Domain) → SELECT_IN_AGA(X, Domain, NewDomain)
SELECT_IN_AGA(X, .(Y, R), .(Y, Rest)) → U23_AGA(X, Y, R, Rest, select_in_aga(X, R, Rest))
SELECT_IN_AGA(X, .(Y, R), .(Y, Rest)) → SELECT_IN_AGA(X, R, Rest)
U21_AG(X, Rest, Domain, select_out_aga(X, Domain, NewDomain)) → U22_AG(X, Rest, Domain, domain_in_ag(Rest, NewDomain))
U21_AG(X, Rest, Domain, select_out_aga(X, Domain, NewDomain)) → DOMAIN_IN_AG(Rest, NewDomain)
U15_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_a(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))) → U16_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_a(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, [])))))))
U15_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_a(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))) → HOUSES_IN_A(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))
U16_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_a(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))) → U17_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_in_a(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, [])))))))
U16_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_a(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))) → HOUSES_IN_A(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))
U17_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_out_a(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))) → U18_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_in_a(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, [])))))))
U17_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_out_a(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))) → HOUSES_IN_A(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))
U18_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_out_a(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))) → U19_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_in_a(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, [])))))))
U18_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_out_a(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))) → HOUSES_IN_A(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, []))))))

The TRS R consists of the following rules:

zebra_in_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) → U1_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_in_aa(Englishman, Red))
eq_in_aa(X, X) → eq_out_aa(X, X)
U1_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_out_aa(Englishman, Red)) → U2_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_in_aa(Spaniard, Dog))
U2_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_out_aa(Spaniard, Dog)) → U3_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_in_aa(Green, Coffee))
U3_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_out_aa(Green, Coffee)) → U4_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_in_aa(Ukrainian, Tea))
U4_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_out_aa(Ukrainian, Tea)) → U5_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_in_aa(Green, Ivory))
to_the_right_in_aa(fifth, fourth) → to_the_right_out_aa(fifth, fourth)
to_the_right_in_aa(fourth, third) → to_the_right_out_aa(fourth, third)
to_the_right_in_aa(third, second) → to_the_right_out_aa(third, second)
to_the_right_in_aa(second, first) → to_the_right_out_aa(second, first)
U5_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_out_aa(Green, Ivory)) → U6_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_in_aa(Winston, Snails))
U6_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_out_aa(Winston, Snails)) → U7_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_in_aa(Kool, Yellow))
U7_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_out_aa(Kool, Yellow)) → U8_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_in_ag(Milk, third))
eq_in_ag(X, X) → eq_out_ag(X, X)
U8_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_out_ag(Milk, third)) → U9_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_in_ag(Norwegian, first))
U9_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_out_ag(Norwegian, first)) → U10_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_in_aa(Fox, Chesterfield))
next_to_in_aa(fifth, fourth) → next_to_out_aa(fifth, fourth)
next_to_in_aa(fourth, fifth) → next_to_out_aa(fourth, fifth)
next_to_in_aa(fourth, third) → next_to_out_aa(fourth, third)
next_to_in_aa(third, fourth) → next_to_out_aa(third, fourth)
next_to_in_aa(third, second) → next_to_out_aa(third, second)
next_to_in_aa(second, third) → next_to_out_aa(second, third)
next_to_in_aa(second, first) → next_to_out_aa(second, first)
next_to_in_aa(first, second) → next_to_out_aa(first, second)
U10_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_out_aa(Fox, Chesterfield)) → U11_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_in_aa(Horse, Kool))
U11_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_out_aa(Horse, Kool)) → U12_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_in_aa(Lucky, Juice))
U12_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_out_aa(Lucky, Juice)) → U13_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_in_aa(Japanese, Parliament))
U13_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_out_aa(Japanese, Parliament)) → U14_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_in_ga(Norwegian, Blue))
next_to_in_ga(fifth, fourth) → next_to_out_ga(fifth, fourth)
next_to_in_ga(fourth, fifth) → next_to_out_ga(fourth, fifth)
next_to_in_ga(fourth, third) → next_to_out_ga(fourth, third)
next_to_in_ga(third, fourth) → next_to_out_ga(third, fourth)
next_to_in_ga(third, second) → next_to_out_ga(third, second)
next_to_in_ga(second, third) → next_to_out_ga(second, third)
next_to_in_ga(second, first) → next_to_out_ga(second, first)
next_to_in_ga(first, second) → next_to_out_ga(first, second)
U14_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_out_ga(Norwegian, Blue)) → U15_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_a(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, [])))))))
houses_in_a(Prop) → U20_a(Prop, domain_in_ag(Prop, .(first, .(second, .(third, .(fourth, .(fifth, [])))))))
domain_in_ag([], X) → domain_out_ag([], X)
domain_in_ag(.(X, Rest), Domain) → U21_ag(X, Rest, Domain, select_in_aga(X, Domain, NewDomain))
select_in_aga(X, .(X, R), R) → select_out_aga(X, .(X, R), R)
select_in_aga(X, .(Y, R), .(Y, Rest)) → U23_aga(X, Y, R, Rest, select_in_aga(X, R, Rest))
U23_aga(X, Y, R, Rest, select_out_aga(X, R, Rest)) → select_out_aga(X, .(Y, R), .(Y, Rest))
U21_ag(X, Rest, Domain, select_out_aga(X, Domain, NewDomain)) → U22_ag(X, Rest, Domain, domain_in_ag(Rest, NewDomain))
U22_ag(X, Rest, Domain, domain_out_ag(Rest, NewDomain)) → domain_out_ag(.(X, Rest), Domain)
U20_a(Prop, domain_out_ag(Prop, .(first, .(second, .(third, .(fourth, .(fifth, []))))))) → houses_out_a(Prop)
U15_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_a(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))) → U16_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_a(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, [])))))))
U16_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_a(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))) → U17_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_in_a(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, [])))))))
U17_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_out_a(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))) → U18_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_in_a(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, [])))))))
U18_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_out_a(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))) → U19_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_in_a(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, [])))))))
U19_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_out_a(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, []))))))) → zebra_out_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

SELECT_IN_AGA(X, .(Y, R), .(Y, Rest)) → SELECT_IN_AGA(X, R, Rest)

The TRS R consists of the following rules:

zebra_in_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) → U1_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_in_aa(Englishman, Red))
eq_in_aa(X, X) → eq_out_aa(X, X)
U1_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_out_aa(Englishman, Red)) → U2_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_in_aa(Spaniard, Dog))
U2_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_out_aa(Spaniard, Dog)) → U3_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_in_aa(Green, Coffee))
U3_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_out_aa(Green, Coffee)) → U4_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_in_aa(Ukrainian, Tea))
U4_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_out_aa(Ukrainian, Tea)) → U5_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_in_aa(Green, Ivory))
to_the_right_in_aa(fifth, fourth) → to_the_right_out_aa(fifth, fourth)
to_the_right_in_aa(fourth, third) → to_the_right_out_aa(fourth, third)
to_the_right_in_aa(third, second) → to_the_right_out_aa(third, second)
to_the_right_in_aa(second, first) → to_the_right_out_aa(second, first)
U5_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_out_aa(Green, Ivory)) → U6_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_in_aa(Winston, Snails))
U6_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_out_aa(Winston, Snails)) → U7_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_in_aa(Kool, Yellow))
U7_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_out_aa(Kool, Yellow)) → U8_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_in_ag(Milk, third))
eq_in_ag(X, X) → eq_out_ag(X, X)
U8_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_out_ag(Milk, third)) → U9_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_in_ag(Norwegian, first))
U9_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_out_ag(Norwegian, first)) → U10_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_in_aa(Fox, Chesterfield))
next_to_in_aa(fifth, fourth) → next_to_out_aa(fifth, fourth)
next_to_in_aa(fourth, fifth) → next_to_out_aa(fourth, fifth)
next_to_in_aa(fourth, third) → next_to_out_aa(fourth, third)
next_to_in_aa(third, fourth) → next_to_out_aa(third, fourth)
next_to_in_aa(third, second) → next_to_out_aa(third, second)
next_to_in_aa(second, third) → next_to_out_aa(second, third)
next_to_in_aa(second, first) → next_to_out_aa(second, first)
next_to_in_aa(first, second) → next_to_out_aa(first, second)
U10_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_out_aa(Fox, Chesterfield)) → U11_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_in_aa(Horse, Kool))
U11_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_out_aa(Horse, Kool)) → U12_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_in_aa(Lucky, Juice))
U12_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_out_aa(Lucky, Juice)) → U13_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_in_aa(Japanese, Parliament))
U13_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_out_aa(Japanese, Parliament)) → U14_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_in_ga(Norwegian, Blue))
next_to_in_ga(fifth, fourth) → next_to_out_ga(fifth, fourth)
next_to_in_ga(fourth, fifth) → next_to_out_ga(fourth, fifth)
next_to_in_ga(fourth, third) → next_to_out_ga(fourth, third)
next_to_in_ga(third, fourth) → next_to_out_ga(third, fourth)
next_to_in_ga(third, second) → next_to_out_ga(third, second)
next_to_in_ga(second, third) → next_to_out_ga(second, third)
next_to_in_ga(second, first) → next_to_out_ga(second, first)
next_to_in_ga(first, second) → next_to_out_ga(first, second)
U14_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_out_ga(Norwegian, Blue)) → U15_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_a(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, [])))))))
houses_in_a(Prop) → U20_a(Prop, domain_in_ag(Prop, .(first, .(second, .(third, .(fourth, .(fifth, [])))))))
domain_in_ag([], X) → domain_out_ag([], X)
domain_in_ag(.(X, Rest), Domain) → U21_ag(X, Rest, Domain, select_in_aga(X, Domain, NewDomain))
select_in_aga(X, .(X, R), R) → select_out_aga(X, .(X, R), R)
select_in_aga(X, .(Y, R), .(Y, Rest)) → U23_aga(X, Y, R, Rest, select_in_aga(X, R, Rest))
U23_aga(X, Y, R, Rest, select_out_aga(X, R, Rest)) → select_out_aga(X, .(Y, R), .(Y, Rest))
U21_ag(X, Rest, Domain, select_out_aga(X, Domain, NewDomain)) → U22_ag(X, Rest, Domain, domain_in_ag(Rest, NewDomain))
U22_ag(X, Rest, Domain, domain_out_ag(Rest, NewDomain)) → domain_out_ag(.(X, Rest), Domain)
U20_a(Prop, domain_out_ag(Prop, .(first, .(second, .(third, .(fourth, .(fifth, []))))))) → houses_out_a(Prop)
U15_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_a(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))) → U16_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_a(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, [])))))))
U16_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_a(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))) → U17_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_in_a(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, [])))))))
U17_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_out_a(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))) → U18_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_in_a(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, [])))))))
U18_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_out_a(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))) → U19_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_in_a(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, [])))))))
U19_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_out_a(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, []))))))) → zebra_out_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

SELECT_IN_AGA(X, .(Y, R), .(Y, Rest)) → SELECT_IN_AGA(X, R, Rest)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
SELECT_IN_AGA(x1, x2, x3) = SELECT_IN_AGA(x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

SELECT_IN_AGA(.(Y, R)) → SELECT_IN_AGA(R)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

SELECT_IN_AGA(.(Y, R)) → SELECT_IN_AGA(R)
The graph contains the following edges 1 > 1

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

U21_AG(X, Rest, Domain, select_out_aga(X, Domain, NewDomain)) → DOMAIN_IN_AG(Rest, NewDomain)
DOMAIN_IN_AG(.(X, Rest), Domain) → U21_AG(X, Rest, Domain, select_in_aga(X, Domain, NewDomain))

The TRS R consists of the following rules:

zebra_in_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) → U1_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_in_aa(Englishman, Red))
eq_in_aa(X, X) → eq_out_aa(X, X)
U1_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_out_aa(Englishman, Red)) → U2_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_in_aa(Spaniard, Dog))
U2_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_out_aa(Spaniard, Dog)) → U3_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_in_aa(Green, Coffee))
U3_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_out_aa(Green, Coffee)) → U4_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_in_aa(Ukrainian, Tea))
U4_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_out_aa(Ukrainian, Tea)) → U5_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_in_aa(Green, Ivory))
to_the_right_in_aa(fifth, fourth) → to_the_right_out_aa(fifth, fourth)
to_the_right_in_aa(fourth, third) → to_the_right_out_aa(fourth, third)
to_the_right_in_aa(third, second) → to_the_right_out_aa(third, second)
to_the_right_in_aa(second, first) → to_the_right_out_aa(second, first)
U5_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_out_aa(Green, Ivory)) → U6_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_in_aa(Winston, Snails))
U6_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_out_aa(Winston, Snails)) → U7_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_in_aa(Kool, Yellow))
U7_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_out_aa(Kool, Yellow)) → U8_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_in_ag(Milk, third))
eq_in_ag(X, X) → eq_out_ag(X, X)
U8_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_out_ag(Milk, third)) → U9_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_in_ag(Norwegian, first))
U9_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_out_ag(Norwegian, first)) → U10_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_in_aa(Fox, Chesterfield))
next_to_in_aa(fifth, fourth) → next_to_out_aa(fifth, fourth)
next_to_in_aa(fourth, fifth) → next_to_out_aa(fourth, fifth)
next_to_in_aa(fourth, third) → next_to_out_aa(fourth, third)
next_to_in_aa(third, fourth) → next_to_out_aa(third, fourth)
next_to_in_aa(third, second) → next_to_out_aa(third, second)
next_to_in_aa(second, third) → next_to_out_aa(second, third)
next_to_in_aa(second, first) → next_to_out_aa(second, first)
next_to_in_aa(first, second) → next_to_out_aa(first, second)
U10_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_out_aa(Fox, Chesterfield)) → U11_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_in_aa(Horse, Kool))
U11_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_out_aa(Horse, Kool)) → U12_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_in_aa(Lucky, Juice))
U12_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_out_aa(Lucky, Juice)) → U13_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_in_aa(Japanese, Parliament))
U13_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_out_aa(Japanese, Parliament)) → U14_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_in_ga(Norwegian, Blue))
next_to_in_ga(fifth, fourth) → next_to_out_ga(fifth, fourth)
next_to_in_ga(fourth, fifth) → next_to_out_ga(fourth, fifth)
next_to_in_ga(fourth, third) → next_to_out_ga(fourth, third)
next_to_in_ga(third, fourth) → next_to_out_ga(third, fourth)
next_to_in_ga(third, second) → next_to_out_ga(third, second)
next_to_in_ga(second, third) → next_to_out_ga(second, third)
next_to_in_ga(second, first) → next_to_out_ga(second, first)
next_to_in_ga(first, second) → next_to_out_ga(first, second)
U14_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_out_ga(Norwegian, Blue)) → U15_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_a(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, [])))))))
houses_in_a(Prop) → U20_a(Prop, domain_in_ag(Prop, .(first, .(second, .(third, .(fourth, .(fifth, [])))))))
domain_in_ag([], X) → domain_out_ag([], X)
domain_in_ag(.(X, Rest), Domain) → U21_ag(X, Rest, Domain, select_in_aga(X, Domain, NewDomain))
select_in_aga(X, .(X, R), R) → select_out_aga(X, .(X, R), R)
select_in_aga(X, .(Y, R), .(Y, Rest)) → U23_aga(X, Y, R, Rest, select_in_aga(X, R, Rest))
U23_aga(X, Y, R, Rest, select_out_aga(X, R, Rest)) → select_out_aga(X, .(Y, R), .(Y, Rest))
U21_ag(X, Rest, Domain, select_out_aga(X, Domain, NewDomain)) → U22_ag(X, Rest, Domain, domain_in_ag(Rest, NewDomain))
U22_ag(X, Rest, Domain, domain_out_ag(Rest, NewDomain)) → domain_out_ag(.(X, Rest), Domain)
U20_a(Prop, domain_out_ag(Prop, .(first, .(second, .(third, .(fourth, .(fifth, []))))))) → houses_out_a(Prop)
U15_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_a(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))) → U16_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_a(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, [])))))))
U16_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_a(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))) → U17_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_in_a(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, [])))))))
U17_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_out_a(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))) → U18_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_in_a(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, [])))))))
U18_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_out_a(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))) → U19_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_in_a(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, [])))))))
U19_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_out_a(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, []))))))) → zebra_out_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

U21_AG(X, Rest, Domain, select_out_aga(X, Domain, NewDomain)) → DOMAIN_IN_AG(Rest, NewDomain)
DOMAIN_IN_AG(.(X, Rest), Domain) → U21_AG(X, Rest, Domain, select_in_aga(X, Domain, NewDomain))

The TRS R consists of the following rules:

select_in_aga(X, .(X, R), R) → select_out_aga(X, .(X, R), R)
select_in_aga(X, .(Y, R), .(Y, Rest)) → U23_aga(X, Y, R, Rest, select_in_aga(X, R, Rest))
U23_aga(X, Y, R, Rest, select_out_aga(X, R, Rest)) → select_out_aga(X, .(Y, R), .(Y, Rest))

The argument filtering Pi contains the following mapping:
select_in_aga(x1, x2, x3) = select_in_aga(x2)
.(x1, x2) = .(x1, x2)
select_out_aga(x1, x2, x3) = select_out_aga(x1, x3)
U23_aga(x1, x2, x3, x4, x5) = U23_aga(x2, x5)
DOMAIN_IN_AG(x1, x2) = DOMAIN_IN_AG(x2)
U21_AG(x1, x2, x3, x4) = U21_AG(x4)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ RuleRemovalProof

Q DP problem:
The TRS P consists of the following rules:

U21_AG(select_out_aga(X, NewDomain)) → DOMAIN_IN_AG(NewDomain)
DOMAIN_IN_AG(Domain) → U21_AG(select_in_aga(Domain))

The TRS R consists of the following rules:

select_in_aga(.(X, R)) → select_out_aga(X, R)
select_in_aga(.(Y, R)) → U23_aga(Y, select_in_aga(R))
U23_aga(Y, select_out_aga(X, Rest)) → select_out_aga(X, .(Y, Rest))

The set Q consists of the following terms:

select_in_aga(x0)
U23_aga(x0, x1)

We have to consider all (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

DOMAIN_IN_AG(Domain) → U21_AG(select_in_aga(Domain))

Strictly oriented rules of the TRS R:

select_in_aga(.(X, R)) → select_out_aga(X, R)
U23_aga(Y, select_out_aga(X, Rest)) → select_out_aga(X, .(Y, Rest))

Used ordering: POLO with Polynomial interpretation [25]:

POL(.(x₁, x₂)) = 1 + x₁ + 2·x₂
POL(DOMAIN_IN_AG(x₁)) = 2 + 2·x₁
POL(U21_AG(x₁)) = 1 + x₁
POL(U23_aga(x₁, x₂)) = 2 + 2·x₁ + 2·x₂
POL(select_in_aga(x₁)) = 2·x₁
POL(select_out_aga(x₁, x₂)) = 1 + 2·x₁ + 2·x₂

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ RuleRemovalProof

                          ↳ QDP

                            ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

U21_AG(select_out_aga(X, NewDomain)) → DOMAIN_IN_AG(NewDomain)

The TRS R consists of the following rules:

select_in_aga(.(Y, R)) → U23_aga(Y, select_in_aga(R))

The set Q consists of the following terms:

select_in_aga(x0)
U23_aga(x0, x1)

We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 1 less node.